\begin{tabbing}
$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]Trans($T$;$x$,$y$.$R$($x$,$y$))
\\[0ex]$\Rightarrow$ \=($\forall$$L$:($T$ List).\+
\\[0ex]($\forall$$i$:\{0..($\parallel$$L$$\parallel$ {-} 1)$^{-}$\}. $R$($L$[$i$],$L$[($i$+1)]))
\\[0ex]$\Rightarrow$ (($\neg$($\uparrow$null($L$))) $\Rightarrow$ $R$(last($L$),hd($L$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$$\in$$L$. $\forall$$b$$\in$$L$. $R$($a$,$b$)))
\-
\end{tabbing}